a:, n:. (-(a rem n)) = ((-a) rem n) 

latex

Up	int 2, int 2
Definitions	t  T, x:A. B(x), , P  Q, P & Q, P  Q, P  Q, , False, {...i}, , A, A  B, P  Q, Dec(P), , a  b  T
Lemmas	int nzero wf, decidable le, rem 2 to 1, rem 3 to 1, rem 4 to 1, minus functionality wrt eq, le wf